COMMENT ⊗   VALID 00002 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002	.require "let.pub" source
C00004 ENDMK
C⊗;
.require "let.pub" source
.font D "Grkl30"
.font E "sup"
∂AIL A. Nozaki↓ICU↓Osawa 3-10-2↓Mitaka, Tokyo↓181 JAPAN∞

Dear Mr. Nozaki:

	I have read and agree with your neat proof of the termination
of the Takeuchi function.  I hope to use it as an example the next
time I teach about termination of recursive programs.

	I have always supposed that this kind of proof could be made
conveniently by defining a rank function and proving that the
referred cases of the function are of lower rank.  In the present
case it would seem that we would use induction up to %Dw%E2%1
and that the coefficient of omega would be your %2u(x,y,z)%1 and the 
linear term would be a conditional expression depending on your case analysis.
We will explore whether the proof can be conveniently expressed in
that way and the role of your inner inductive proof.  Should any of
us write anything about it, I'll send it to you.

	The main interest of the Takeuchi function for me is to be
able to write computer checkable proofs of the properties of
recursive programs in a neat way, and the Takeuchi function certainly
provides a nice example.

.sgn